Nuprl Definition : add_grp_of_rng
13,42
postcript
pdf
r
+gp == <|
r
|, =
,
, +
r
, 0, -
r
>
latex
clarification:
r
+gp == <|
r
|, =
r
,
r
, +
r
, 0
r
, -
r
>
latex
Up
rings
1
Wellformedness Lemmas
add
grp
of
rng
wf
,
add
grp
of
rng
wf
a
,
add
grp
of
rng
wf
b
Definitions
|
r
|
,
=
,
,
+
r
,
0
,
-
r
origin
+gp == <|r|, =
, 
, +r, 0, -r>
+gp == <|r|, =r, r, +r, 0r, -r> +gp == <|r|, =, , +r, 0, -r>
+gp == <|r|, =r, r, +r, 0r, -r>